-- Model of the problem of Bob and Alice Party. Bob and Alice invited other
-- three couples to a party at their place. Some were polite, some were not,
-- so some shook hands with other people, but not everyone did so. Obviously,
-- no one shook hands with the partner he/she came with.
-- Alice asked everyone how many people he/she shook hands with, obtaining
-- all different answers. How many people Bob shook hands with?
-- Author of the model (not the problem): Nazareno Aguirre
-- 2008.

-- The important information about people is the partner and who each person 
-- shook hands with. 
abstract sig Person { 
	partner: one Person,
	shookHands: set Person
}
{
    -- no one shook hands with his/her partner
	this !in shookHands and partner !in shookHands
}

-- partner is symmetric. No one can be his/her own partner
fact partnerIsSymmetricAndNotReflexive {
	partner = ~partner and
	no (iden & partner)
}

-- Alice is Bob's partner, and vice versa
fact BobIsAlicePartner {
	Bob.partner = Alice
}

-- shookHands is symmetric.
fact shookHandsIsSymmetric {
	shookHands = ~ shookHands
}

-- Alice asked everyone how many people he/she shook hands with, obtaining
-- all different answers.
fact allDiffs {
	all disj p1, p2: Person-Alice | #p1.shakedHands != #p2.shakedHands 
}

pred show[] { }

run show
